safety($A$;${\it tr}$.$P$(${\it tr}$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$${\it tr}_{1}$:$A$ List, ${\it tr}_{2}$:$A$ List. ${\it tr}_{1}$ $\leq$ ${\it tr}_{2}$ $\in$ $A$ List $\Rightarrow$ $P$(${\it tr}_{2}$) $\Rightarrow$ $P$(${\it tr}_{1}$)